Theorem mp3an1 901

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an1.1	⊢ φ
mp3an1.2	⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Assertion

Ref	Expression
mp3an1	⊢ ((ψ ⋀ χ) → θ)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ φ
2		mp3an1.2	. . 3 ⊢ ((φ ⋀ ψ ⋀ χ) → θ)
3	2	3expb 833	. 2 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
4	1, 3	mpan 694	1 ⊢ ((ψ ⋀ χ) → θ)

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 774

This theorem is referenced by:  mp3an12 904  mp3an1i 907  mp3anl1 908  mp3an 914  onint 3001  brelrn 3339  tfrlem9 3910  oaord1 4175  oaword2 4177  oawordeulem 4178  oa00 4183  omword1 4194  omword2 4195  omlimcl 4199  unfilem2 4531  fodomb 4780  brdom3 4781  brdom7disj 4784  brdom6disj 4785  mulclpi 5001  mulidpq 5049  halfpq 5062  cnegext 5328  negeu 5335  muladd11t 5402  xrre2t 5551  ltaddpost 5632  addge01t 5653  receu 5678  recclt 5692  div0t 5731  recdiv2t 5760  rerecclt 5767  ltmul12it 5805  lemul12itOLD 5807  lemul12it 5808  mulgt1t 5809  lediv12it 5852  ledivp1t 5861  nngt1ne1t 5900  nnaddm1clt 5913  8th4div3 5986  infm3 6009  infmrcl 6024  xrub 6035  supxrre 6038  nn0ltp1let 6082  gtndivt 6148  nn0ind 6168  qbtwnxr 6225  qsqueeze 6226  om2uzran 6245  ser1mono 6282  elioc2t 6330  elico2t 6331  elicc2t 6332  elfz2nn0t 6435  expubndt 6547  le2sqit 6571  bernneq 6591  sqr2irr 6667  imret 6718  cau4i 6863  cau5 6864  cvg3 6868  faclbnd5 6898  fsumcom 6974  climubi 7097  climsup 7099  caucvglem6 7106  caucvg 7107  serzf0 7113  cvgcmp 7128  cvgcmpub 7129  isumnn0nn 7150  geoser 7177  georeclim 7183  geoisumr 7186  0.999... 7189  cvgratlem4 7196  efcltlem1 7254  erelem3 7271  efaddlem6 7293  efaddlem15 7302  ef01tllem2 7334  effsumle 7346  efi4pt 7385  cos2tt 7413  sin01bndlem3 7419  cos01bndlem3 7421  sin01gt0 7426  cos01gt0 7427  demoivre 7434  znnen 7453  infpn2 7460  iooretop 7609  metxplem1 7778  metxplem2 7779  metxplem3 7780  metxp 7786  bl2in 7795  methausi 7833  xplmi 7923  xpcn 7926  bcthlem3 7951  bcthlem9 7957  bcthlem20 7968  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  isgrpi 7992  ghgrpilem3 8087  ghgrpilem4 8088  ghsubgi 8090  imsmetlem 8274  nmcnilem 8285  va1cnlem 8292  sm1cnilem 8294  ipval2 8304  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem5 8324  ip1cnilem6 8325  lnocoi 8365  nmlno0lem 8398  nmblolbii 8403  blometi 8407  blocnilem 8408  blocni 8409  ipasslem1 8434  ipasslem2 8435  ipasslem4 8437  ipasslem5 8438  ipasslem8 8441  ipblnfi 8460  ip2eqi 8461  ubthlem6 8478  ubthlem7 8479  ubthlem8 8480  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  minveclem9 8497  minveclem15 8503  minveclem16 8504  minveclem18 8506  minveclem19 8507  minveclem21 8509  minveclem25 8513  minveclem27 8515  minveclem28 8516  minveclem30 8518  minveclem31 8519  minveclem35 8523  minveclem36 8524  minveclem37 8525  minveclem38 8526  minveceu 8527  htthlem6 8568  htthlem10 8572  sincosq1eq 8645  efghgrpilem 8653  efifolem5 8660  shftefif1olem 8680  logeftb 8703  h2hmetdval 8787  axhvcom 8792  axhis1 8803  axhis4 8806  hvm1negt 8840  hvsub4t 8845  hvsubdistr2t 8856  hv2timest 8867  hvsubcant 8880  hvsubcan2t 8881  his2subt 8897  his6t 8904  norm-it 8935  normpyct 8952  hhip 8983  hhph 8984  hhcms 9011  hhssabl 9071  hhssnv 9073  hhshsslem2 9077  hhssmetdval 9088  hhsscms 9089  projlem26 9150  projlem30 9154  shscl 9219  shunss 9275  h1datom 9444  osumlem6 9523  homulid2t 9666  honegdit 9675  ho2timest 9685  nmopge0t 9774  nmopgt0t 9775  nmfnge0t 9790  lnopadd 9834  lnopmul 9835  lnopsub 9837  hmopbdopHIL 9851  nmbdoplb 9887  nmcoplb 9896  nmophm 9899  lnopcon 9901  lnfnadd 9910  lnfnsub 9913  nmbdfnlb 9916  nmcfnlb 9925  lnfncon 9928  cnlnadjlem2 9939  cnlnadjlem7 9944  adjbdlnt 9954  nmoptri 9965  nmopco 9966  adjco 9971  nmopcoadj 9972  bracnlnvalt 9985  leopmult 10005  hmopidmchlem 10016  hmopidmpj 10018  pjima 10042  sto2 10102  atcveq0 10212  atcv0eq 10243  atoml 10246  atcvat 10250  atcvat3 10260  ghomgrpilem2 10320  ghomsn 10322  cayleylem2 10344  nndivlub 10358

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776

Copyright terms: Public domain