Theorem mp3an 1491

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	⊢ 𝜑
mp3an.2	⊢ 𝜓
mp3an.3	⊢ 𝜒
mp3an.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an	⊢ 𝜃

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 ⊢ 𝜓
2		mp3an.3	. 2 ⊢ 𝜒
3		mp3an.1	. . 3 ⊢ 𝜑
4		mp3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	3, 4	mp3an1 1478	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 705	1 ⊢ 𝜃

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  el3v  3462  raltp  4666  rextp  4667  opthhausdorff  5494  fununiq  6572  funopg  6591  feq12i  6721  ftp  7182  caovass  7642  caovdi  7661  ordom  7908  mptexw  7986  ofmres  8017  sbcoteq1a  8084  mpoexw  8113  xpord3lem  8190  omopthlem1  8693  omopthlem2  8694  omopthi  8695  on2recsfn  8701  xpcomen  9112  snnen2o  9261  unfilem3  9324  hartogs  9562  card2on  9572  unwf  9842  inlresf1  10020  inrresf1  10022  tskwe  10055  alephsmo  10205  dfac4  10225  dfac2a  10232  ackbij1lem13  10333  axdc2lem  10550  axcclem  10559  ondomon  10671  cfpwsdom  10693  pwfseqlem2  10768  pwfseqlem3  10769  1lt2pi  11014  addassi  11343  mulassi  11344  adddii  11345  adddiri  11346  lttri  11460  lelttri  11461  ltletri  11462  letri  11463  ltadd2i  11465  mul02lem2  11511  addrid  11514  addcani  11527  addcan2i  11528  mul12i  11529  mul32i  11530  add12i  11557  add32i  11558  subaddi  11669  subadd2i  11670  subsub23i  11672  addsubassi  11673  addsubi  11674  subcani  11675  subcan2i  11676  pnncani  11677  subdii  11789  subdiri  11790  ltadd1i  11894  leadd1i  11895  leadd2i  11896  ltsubaddi  11897  lesubaddi  11898  ltsubadd2i  11899  lesubadd2i  11900  ltaddsubi  11901  mulcani  11979  div23i  12099  div11i  12100  3halfnz  12802  mpoaddex  13140  addex  13141  mpomulex  13142  mulex  13143  unirnioo  13604  ioorebas  13606  xnn0xrge0  13661  fldiv4lem1div2  14001  uzenom  14131  nnenom  14147  seqexw  14184  m1expcl2  14252  i4  14372  expnass  14376  faclbnd4lem1  14461  bcn1  14481  hashfxnn0  14505  ccat2s1p1  14802  ccat2s1p2  14803  cats1fvn  15034  cats1fv  15035  cats1cat  15037  cats2cat  15038  wrdlen3s3  15126  sgnrn  15277  sgnclre  15281  abs3difi  15603  0.999...  16076  bpoly3  16250  ef01bndlem  16378  cos1bnd  16381  cos2bnd  16382  sin4lt0  16389  rpnnen2lem3  16410  rpnnen2lem11  16418  rpnnen  16421  rexpen  16422  aleph1irr  16440  3dvdsdec  16528  3dvds2dec  16529  divalglem2  16591  ndvdsi  16608  flodddiv4  16611  gcdaddmlem  16722  bezout  16742  3lcm2e6woprm  16816  6lcm4e12  16817  lcmf0  16835  lcmf2a3a4e12  16848  dec2dvds  17267  modxai  17272  modsubi  17276  gcdi  17277  numexp2x  17282  2exp5  17289  2exp11  17293  ex-chn2  18838  degenmgmnfn  19162  degenmgm  19163  degenmgm2opdm  19164  degenmgm2  19166  0symgefmndeq  19635  pmtrprfval  19728  m1expaddsub  19739  0frgp  20020  staffval  21125  cnfldcj  21714  cnfldds  21717  cnfldfunALT  21720  xrsadd  21723  xrsmul  21724  xrsds  21743  cnmgpid  21762  nn0srg  21770  rge0srg  21771  zring0  21791  pzriprnglem13  21826  pzriprng1ALT  21829  fermltlchr  21862  cnmsgnsubg  21910  psgninv  21915  re0g  21945  ocvfval  21999  frlmbas  22088  mdetrlin  22944  mdetunilem9  22962  leordtval2  23557  iscnp2  23584  nmfval  24934  nmoffn  25057  nmofval  25060  icccld  25112  addcnlem  25211  iimulcn  25286  icopnfhmeo  25291  iccpnfcnv  25292  iccpnfhmeo  25293  xrhmeo  25294  xrhmph  25295  oprpiece1res1  25299  oprpiece1res2  25300  ishtpy  25320  pcoass  25372  cnstrcvs  25489  cncvs  25493  recvs  25494  qcvs  25495  zclmncvs  25496  tcphex  25565  cnfldcusp  25705  resscdrg  25706  reust  25729  recusp  25730  vitalilem4  25959  vitalilem5  25960  mbfdm  25974  dveflem  26326  dvlipcn  26341  c1lip2  26345  dgrid  26610  iaa  26678  iaaOLD  26679  abelthlem3  26787  abelthlem5  26789  abelth  26795  efcn  26797  sinhalfpilem  26819  sincosq1lem  26853  sincosq4sgn  26857  tangtx  26861  sincos4thpi  26869  sincos6thpi  26871  pigt3  26873  pige3ALT  26875  cos0pilt1  26887  logi  26942  relogcn  26993  dvlog2lem  27007  dvlog2  27008  logtayl  27015  logtayl2  27017  cxpsqrtlem  27057  cxpsqrt  27058  2irrexpq  27086  cxpcn2  27101  cxpcn3  27103  logblog  27147  2logb9irr  27150  2logb3irr  27152  2logb9irrALT  27153  sqrt2cxp2logb9e3  27154  2irrexpqALT  27155  ang180lem1  27164  ang180lem2  27165  1cubrlem  27196  mcubic  27202  quart1lem  27210  quart1  27211  reasinsin  27251  atancj  27265  efiatan  27267  atantan  27278  atanbndlem  27280  atan1  27283  atancn  27291  atantayl2  27293  log2cnv  27299  log2tlbnd  27300  log2ublem1  27301  log2ublem2  27302  log2ub  27304  efrlim  27324  scvxcvx  27340  1sgm2ppw  27554  ppiub  27558  bclbnd  27634  bposlem8  27645  lgsdir2lem1  27679  lgsdir2lem5  27683  lgseisenlem1  27729  lgseisenlem2  27730  lgsquadlem1  27734  chebbnd1  27826  dchrvmasumlem2  27852  norecfn  28359  norec2fn  28369  addsproplem2  28383  addsproplem6  28387  addbdaylem  28430  neg1s  28440  negsproplem2  28442  mulsproplem2  28530  mulsproplem3  28531  mulsproplem5  28533  mulsproplem6  28534  mulsproplem7  28535  mulsproplem8  28536  mulsproplem13  28541  mulsproplem14  28542  0zs  28801  zseo  28835  twocut  28836  bdaypw2n0bndlem  28876  bdaypw2bnd  28878  bdayfinbndlem1  28880  z12bdaylem2  28884  istrkg3ld  28950  trgcgrg  29005  ax5seglem7  29540  axlowdimlem6  29552  axlowdimlem8  29554  axlowdimlem11  29557  elntg2  29590  lfuhgr2  29754  cusgrsizeindb1  30058  vtxdginducedm1  30151  0grrusgr  30187  erclwwlktr  30640  erclwwlkntr  30689  wlk2v2e  30785  upgr3v3e3cycl  30808  konigsberglem1  30880  konigsberglem2  30881  konigsberglem3  30882  konigsberglem5  30884  ex-fl  31075  ex-mod  31077  ex-hash  31081  ex-lcm  31086  0vfval  31235  smcnlem  31326  lnocoi  31386  nmlno0lem  31422  nmblolbii  31428  blocnilem  31433  blocni  31434  cncph  31448  isph  31451  ip0i  31454  ip1ilem  31455  ip2i  31457  ipdirilem  31458  ipasslem7  31465  ipasslem8  31466  ipasslem9  31467  ipasslem10  31468  ipasslem11  31469  ip2dii  31473  pythi  31479  siilem1  31480  siilem2  31481  siii  31482  hvmulassi  31675  hvmulcomi  31676  hvdistr1i  31680  hvsubdistr1i  31681  hvassi  31682  hvadd32i  31683  hvsubassi  31684  hvsub32i  31685  normlem0  31738  normlem8  31746  normlem9  31747  bcseqi  31749  polid2i  31786  hhph  31807  hlim0  31864  shscli  31946  shlessi  32006  shlej1i  32007  omlsilem  32031  shlubi  32044  h1de2i  32182  pjadjii  32303  pjaddii  32304  pjmulii  32306  pjdifnormii  32312  pjcji  32313  hoaddsubassi  32449  eigrei  32463  eigposi  32465  eigorthi  32466  adj0  32623  lnopeq0lem1  32634  lnopunilem1  32639  lnophmlem2  32646  nmcexi  32655  nmcopexi  32656  lnfn0i  32671  nmcfnexi  32680  mdexchi  32964  xppreima2  33314  dp2clq  33514  dp2lt  33518  dp2ltc  33520  dpexpp1  33541  dpmul  33546  dpmul4  33547  elxrge02  33565  xrge0adddir  33646  psgnid  33725  cnmsgn0g  33774  altgnsg  33777  xrnarchi  33812  xrge0slmod  33976  znfermltl  33989  ccfldextdgrr  34371  cos9thpiminplylem4  34484  cos9thpiminplylem5  34485  raddcn  34628  xrge0iifcnv  34632  xrge0iifiso  34634  xrge0iifhmeo  34635  xrge0iifhom  34636  xrge0iifmhm  34638  xrge0mulc1cn  34640  lmlimxrge0  34647  pnfneige0  34650  lmxrge0  34651  zringnm  34657  rezh  34668  qqh0  34683  qqh1  34684  qqhucn  34691  esumpinfval  34772  hashf2  34783  esumcvg  34785  br2base  34968  sxbrsigalem3  34971  dya2iocbrsiga  34974  dya2icobrsiga  34975  sxbrsigalem1  34984  sxbrsigalem2  34985  sxbrsigalem4  34986  sxbrsigalem5  34987  sxbrsiga  34989  ballotlem2  35188  ballotlem4  35198  ballotlemi1  35202  ballotth  35237  signstf  35262  itgexpif  35302  chtvalz  35325  hgt750lemd  35344  hgt750lem  35347  tgoldbachgnn  35355  jk1k2k3  36017  subfacp1lem1  36110  subfacp1lem6  36116  kur14lem6  36142  cvmliftlem4  36219  satf0suc  36307  problem4  36599  quad3  36601  iexpire  36677  fvtransport  36974  ttcid  37457  dfttc2g  37471  bj-minftyccb  38337  taupilem2  38434  iccioo01  38441  1oequni2o  38482  finxp1o  38506  finxpreclem4  38508  cos2h  38725  tan2h  38726  poimirlem9  38738  poimirlem27  38756  poimirlem28  38757  ismblfin  38770  mbfposadd  38776  ftc1anclem5  38806  asindmre  38812  dvasin  38813  dvacos  38814  rrnval  38952  dihjatcclem4  42669  lcmineqlem12  43281  fisdomnn  43486  subex  43489  absex  43490  cjex  43491  cxpi11d  43585  redvmptabs  43602  readvrec  43604  sn-00idlem2  43641  sn-00id  43643  remul02  43647  rabren3dioph  44013  jm2.27dlem2  44208  rmydioph  44212  rmxdioph  44214  expdiophlem2  44220  expdioph  44221  arearect  44407  areaquad  44408  2omomeqom  44495  omnord1ex  44496  corclrcl  44897  corcltrcl  44929  dffrege76  45129  k0004val0  45344  lhe4.4ex1a  45503  binomcxplemdvbinom  45527  binomcxplemnotnn0  45530  ax6e2ndeqALT  46102  sineq0ALT  46108  nregmodelf1o  46198  pnfel0pnf  46743  lptioo2cn  46858  limsup10ex  46986  liminf10ex  46987  icccncfext  47100  itgsin0pilem1  47163  itgsbtaddcnst  47195  stoweidlem13  47226  wallispilem2  47279  wallispilem4  47281  wallispi2lem1  47284  stirlinglem13  47299  dirkerper  47309  dirkertrigeqlem3  47313  dirkeritg  47315  dirkercncflem1  47316  dirkercncflem4  47319  fourierdlem42  47362  fourierdlem62  47381  fourierdlem102  47421  fourierdlem103  47422  fourierdlem104  47423  fourierdlem114  47433  sqwvfoura  47441  fourierswlem  47443  fouriersw  47444  smfmullem4  48007  sqrtnnaa  48116  sqrtnzqaa  48117  goldpolyfactor  48130  goldracos5teq  48135  goldratmolem2  48136  goldratval  48139  sqrtnpoly  48146  ceil5half3  48619  8mod5e3  48639  fmtnoprmfac2lem1  48854  fmtno4prm  48863  3exp4mod41  48904  41prothprmlem2  48906  ppivalnn4  48915  6gbe  49072  7gbow  49073  8gbe  49074  9gbo  49075  11gbo  49076  sbgoldbalt  49082  nnsum4primesevenALTV  49102  usgrexmpl2nb0  49332  usgrexmpl2nb3  49335  gpg3nbgrvtx0  49377  gpg3nbgrvtx0ALT  49378  gpg3nbgrvtx1  49379  gpg5grlim  49394  gpg5grlic  49395  0nodd  49470  oddinmgm  49475  2zrng0  49544  zlmodzxz0  49671  zlmodzxzequa  49811  zlmodzxzequap  49814  zlmodzxzldeplem3  49817  nnlog2ge0lt1  49881  blen1  49899  blen2  49900  nnolog2flm1  49905  ackval42  50011  ehl2eudisval0  50041  i0oii  50237  io1ii  50238  sepfsepc  50245  rescofuf  50411  setc1ohomfval  50831  setc1ocofval  50832