Theorem 3expia 1139

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 462	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ 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:  ad5ant125OLD  1391  mp3an3  1479  3gencl  3493  vtocl3gaf  3539  vtocl3ga  3540  moi  3676  disji  5088  disjord  5092  3optocl  5752  sossfld  6179  f1oresrab  7121  f1cdmsn  7283  soisores  7328  isomin  7338  isofrlem  7341  ovmpos  7561  ov2gf  7562  ndmovord  7604  nnsuc  7880  poxp  8126  frpoins3xp3g  8139  brtpos  8233  dfsmo2  8336  smoiun  8350  smoord  8354  smogt  8356  omeulem1  8569  omeu  8572  oewordi  8579  uniinqs  8797  mapvalg  8835  pmvalg  8836  elmapg  8838  xpdom3  9073  mapdom3  9147  sdomdomtrfi  9195  domsdomtrfi  9196  php  9201  php3  9203  nndomog  9207  onomeneq  9208  sucdom  9214  unxpdomlem3  9228  isinf  9235  f1finf1o  9243  isfinite2  9268  prfi  9293  ordiso  9488  cnfcom3clem  9684  r111  9757  tskwe  9955  pr2ne  10008  infxpenlem  10016  dfac8alem  10032  infdif  10210  infdif2  10211  cff1  10260  coflim  10263  cfslbn  10269  cfslb2n  10270  cofsmo  10271  cfsmolem  10272  cfcoflem  10274  fin23lem27  10330  isf32lem9  10363  isf34lem6  10382  axcc2lem  10438  domtriomlem  10444  axdc4lem  10457  zorn2lem2  10499  axdclem2  10522  konigthlem  10577  gchen1  10634  gchen2  10635  gchpwdom  10679  gchaleph  10680  winainflem  10702  tskcard  10790  gruiun  10808  gruen  10821  intgru  10823  grudomon  10826  grur1a  10828  grutsk1  10830  nqereu  10938  nqereq  10944  ltsonq  10978  prlem934  11042  reclem3pr  11058  1re  11232  axsup  11309  addlid  11417  recex  11870  lemul1a  12093  lt2msq  12124  fimaxre2  12184  indpi1  12256  zdiv  12691  zextlt  12695  prime  12702  uzind2  12714  fzind  12719  lbzbi  12985  qbtwnxr  13252  qextltlem  13254  xralrple  13257  xltneg  13269  xlt2add  13312  supxrgtmnf  13381  ixxub  13419  ixxlb  13420  ioo0  13423  ico0  13444  ioc0  13445  icc0  13446  iocssre  13480  icossre  13481  iccssre  13482  fzen  13595  expclzlem  14147  expaddz  14170  expmulz  14172  hashgadd  14441  hashunsngx  14457  hashgt23el  14489  elovmpowrd  14623  pfxnd0  14758  ccatopth2  14786  pfxccatin12  14802  cshf1  14881  shftuz  15142  sgn3da  15174  sgnnbi  15177  sgnpbi  15178  cau3lem  15442  caubnd  15446  climuni  15639  lo1resb  15651  o1resb  15653  o1of2  15700  o1add  15701  o1mul  15702  o1sub  15703  ntrivcvgmul  15991  eflt  16205  moddvds  16353  dvdscmulr  16374  dvdsmulcr  16375  dvdsle  16400  divalglem8  16490  divalgb  16494  ndvdssub  16499  bitsfzo  16525  gcdcllem1  16589  gcdcllem3  16591  dvdsgcd  16634  nn0rppwr  16651  nn0expgcd  16654  lcmgcdlem  16696  lcmfeq0b  16720  qredeu  16748  isprm3  16773  prmdvdsexpr  16808  prmexpb  16810  eulerthlem2  16873  fermltl  16875  coprimeprodsq  16900  pythagtrip  16926  pcprendvds  16932  pcpremul  16935  pcdvdsb  16961  pc2dvds  16971  4sqlem12  17048  4sqlem18  17054  vdwlem10  17082  cshwshashlem3  17189  xpsrnbas  17657  ismred  17686  mrieqv2d  17727  iscatd  17761  isfuncd  17954  fthestrcsetc  18238  fthsetcestrc  18253  poslubd  18499  dirtr  18690  mulgaddcom  19221  ghmrn  19356  pmtrprfv3  19581  mndodcongi  19670  oddvdsnn0  19671  oddvds  19674  odcl2  19692  odhash3  19703  gexdvds  19711  pgpfi  19732  lsmss1b  19793  lsmss2b  19795  efgsrel  19861  efgred  19875  cntzcmn  19967  cyggenod  20011  lt6abl  20022  gsumcom2  20102  pgpfac1lem2  20204  pgpfac1lem3  20206  dvdsunit  20520  unitmulclb  20522  irredrmul  20568  isabvd  20978  lmodvsdi  21069  lss0cl  21131  islbs3  21342  lbsextlem2  21346  rspprop  21433  xrsdsreclblem  21626  psrbaglefi  22141  mvrf1  22200  coe1fzgsumd  22529  gsummoncoe1  22533  evl1gsumd  22582  scmataddcl  22738  scmatsubcl  22739  mdetunilem9  22842  mdetuni0  22843  mdetmul  22845  m2cpmrngiso  22983  pm2mpf1  23024  opnnei  23345  neindisj2  23348  cncls2  23498  cncls  23499  cnntr  23500  cnpresti  23513  cnprest  23514  lmcnp  23529  isreg2  23602  ordthauslem  23608  unconn  23654  2ndc1stc  23676  kgen2ss  23781  ptclsg  23841  cnmptcom  23904  kqfvima  23956  hmeof1o  23990  fbncp  24065  fbfinnfr  24067  trfbas2  24069  isufil2  24134  ufprim  24135  trufil  24136  filufint  24146  hausflim  24207  flimrest  24209  flimcls  24211  cnpfcf  24267  alexsubALT  24277  tmdgsum  24321  opnsubg  24334  cldsubg  24337  qustgpopn  24346  tsmsxp  24381  blpnf  24623  blssps  24650  blss  24651  blssec  24661  neibl  24727  prdsxmslem2  24755  xrsmopn  25039  metnrm  25089  climcncf  25128  iccpnfhmeo  25173  xrhmeo  25174  bndth  25186  cphsqrtcl3  25415  iscau2  25505  iscmet3lem2  25520  bcthlem5  25556  bcth3  25559  ishl2  25598  ivthlem1  25679  cmmbl  25762  iundisj2  25777  voliunlem2  25779  mbfaddlem  25888  itg2itg1  25964  itg2seq  25970  itg2mulclem  25974  cnplimc  26114  dvres2  26139  deg1nn0clb  26315  deg1lt0  26316  deg1ge  26323  plypf1  26438  plyadd  26443  plymul  26444  coeeu  26451  dgrub2  26461  coeidlem  26463  coeid3  26466  coemullem  26476  coe11  26479  coemulhi  26480  coemulc  26481  dgreq0  26491  dgrlt  26492  dgradd2  26494  vieta1lem2  26543  tanord1  26774  tanord  26775  logccne0  26815  cxpeq0  26915  cxpmul2z  26928  cxpcn3lem  26984  rtprmirr  26997  relogbzcl  27011  angpieqvd  27068  o1cxp  27211  scvxcvx  27222  chtublem  27447  bposlem3  27522  lgsqr  27587  2sqnn  27675  dchrisumlema  27724  dchrisumlem2  27726  ostth2lem3  27871  nosepon  27901  noextenddif  27904  nolesgn2o  27907  nogesgn1o  27909  nosepne  27916  nodense  27928  onnolt  28531  onlts  28532  oniso  28536  bdayn0p1  28634  bdayn0sf1o  28635  tghilberti2  28985  inagswap  29239  f1otrg  29327  brbtwn2  29362  axpasch  29398  axcontlem4  29424  axcontlem5  29425  upgredg2vtx  29598  usgredg2vtxeuALT  29682  sizusglecusg  29923  upgredginwlk  30095  subgrwlk  30148  frgrwopreg1  30798  frgrwopreg2  30799  frgrregorufrg  30806  lpni  30961  ipasslem5  31316  htthlem  31398  omlsii  31884  spansni  32038  spansneleq  32051  elspansn4  32054  sumspansn  32130  homco1  32282  homulass  32283  mdsl0  32791  ssdmd1  32794  ssdmd2  32795  cvdmd  32818  chirredlem2  32872  atdmd  32879  atmd2  32881  disjif  33051  iundisj2f  33063  isoun  33174  preiman0  33182  padct  33189  iocinioc2  33250  iundisj2fi  33268  archiabllem1a  33631  archiabllem2a  33634  slmdvsdi  33655  ordtconnlem1  34434  measinblem  34731  measres  34733  measdivcstALTV  34736  mbfmco2  34776  orvclteinc  34987  bnj605  35416  bnj607  35425  bnj964  35452  bnj1033  35478  bnj1128  35499  bnj1137  35504  bnj1136  35506  bnj1413  35544  bnj60  35571  rankfilimb  35610  r1filim  35612  nelscottrankgt  35632  fineqvac  35642  fineqvnttrclselem3  35649  fineqvnttrclse  35650  vonf1oonfo  35712  cusgredgex  35720  acycgr1v  35728  cvmlift2lem10  35891  msubvrs  36139  wsuclem  36402  dfrdg4  36530  brcolinear2  36638  brsegle2  36689  nn0prpw  36942  ntruni  36946  clsint2  36948  fnessref  36976  fnemeet2  36986  fnejoin2  36988  limsucncmpi  37064  ee7.2aOLD  37080  bj-idreseq  37914  dissneqlem  38094  isbasisrelowllem1  38109  isbasisrelowllem2  38110  icoreclin  38111  poimirlem9  38378  poimirlem30  38399  poimirlem32  38401  areacirc  38462  filbcmb  38490  mettrifi  38507  heiborlem8  38568  heiborlem10  38570  heibor  38571  riscer  38738  igenval2  38816  eldisjim3  39563  eldisjs6  39688  lshpcmp  39861  eqlkr  39972  lkrlsp2  39976  lkrshp  39978  cvrnbtwn2  40148  cvlexch3  40205  cvlexch4N  40206  cvlatexchb1  40207  cvlsupr3  40217  exatleN  40277  cvratlem  40294  atcvrj2b  40305  cvrat3  40315  cvrat4  40316  athgt  40329  ps-1  40350  ps-2  40351  3atlem5  40360  3at  40363  llnneat  40387  llnmlplnN  40412  lplnneat  40418  lplnnelln  40419  islpln2a  40421  lplnriaN  40423  lplnribN  40424  lplnexllnN  40437  2llnjaN  40439  lvolnle3at  40455  lvolneatN  40461  lvolnelln  40462  lvolnelpln  40463  islvol2aN  40465  dalem62  40607  pmapglb2N  40644  pmapglb2xN  40645  lncmp  40656  paddasslem14  40706  paddasslem15  40707  pmod2iN  40722  hlmod1i  40729  pclfinclN  40823  osumcllem8N  40836  pexmidlem4N  40846  pl42lem1N  40852  pl42lem4N  40855  lhpexle1  40881  lhpexle2lem  40882  lhpmcvr5N  40900  lhpmcvr6N  40901  ltrneq  41022  trlnidatb  41050  cdleme0ex2N  41097  cdleme27a  41240  cdleme17d3  41369  cdlemeg46gfre  41405  cdleme48gfv1  41409  cdlemeg49lebilem  41412  cdlemf2  41435  cdlemf  41436  cdlemfnid  41437  trlord  41442  cdlemg31c  41572  cdlemg35  41586  trlcone  41601  tendoeq2  41647  cdlemj3  41696  cdlemk26b-3  41778  cdlemk33N  41782  cdleml3N  41851  cdlemn  42085  dih1dimb2  42114  dihord5apre  42135  dihmeetlem1N  42163  dihglblem5apreN  42164  dihglblem2N  42167  dihglblem3N  42168  dihmeetlem13N  42192  dihmeetlem15N  42194  dihatexv  42211  hdmap14lem12  42752  uzindd  42844  lcmineqlem1  42895  sticksstones1  43012  dvdsexpnn0  43209  frlmfzowrdb  43392  oddcomabszz  43785  jm2.19lem4  43833  fiuneneq  44033  idomsubgmo  44034  omcl2  44174  pwinfi3  44403  gneispa  44970  mnringmulrcld  45066  grumnudlem  45109  ismnushort  45125  binomcxplemnn0  45173  addrcom  45297  int3  45435  suctrALT  45648  suctrALTcf  45744  suctrALT3  45746  chordthmALT  45755  iunconnlem2  45757  relpmin  45775  relpfrlem  45776  stoweidlem26  46854  stoweidlem34  46862  issald  47161  goldbachth  48450  nprmdvdsfacm1  48527  grlimgrtri  48919  nnsgrp  49092  ply1mulgsumlem1  49316  lubsscl  49886  glbsscl  49887