Theorem 3expia 1117

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 1116	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 459	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  ad5ant125  1362  mp3an3  1446  3gencl  3538  moi  3711  disji  5051  disjord  5056  3optocl  5649  sossfld  6045  f1oresrab  6891  soisores  7082  isomin  7092  isofrlem  7095  ovmpos  7300  ov2gf  7301  ndmovord  7340  nnsuc  7599  poxp  7824  brtpos  7903  dfsmo2  7986  smoiun  8000  smoord  8004  smogt  8006  omeulem1  8210  omeu  8213  oewordi  8219  uniinqs  8379  mapvalg  8418  pmvalg  8419  elmapg  8421  xpdom3  8617  mapdom3  8691  php3  8705  unxpdomlem3  8726  isinf  8733  findcard2  8760  isfinite2  8778  ordiso  8982  cnfcom3clem  9170  r111  9206  tskwe  9381  pr2ne  9433  infxpenlem  9441  dfac8alem  9457  infdif  9633  infdif2  9634  cff1  9682  coflim  9685  cfslbn  9691  cfslb2n  9692  cofsmo  9693  cfsmolem  9694  cfcoflem  9696  fin23lem27  9752  isf32lem9  9785  isf34lem6  9804  axcc2lem  9860  domtriomlem  9866  axdc4lem  9879  zorn2lem2  9921  axdclem2  9944  konigthlem  9992  gchen1  10049  gchen2  10050  gchpwdom  10094  gchaleph  10095  winainflem  10117  tskcard  10205  gruiun  10223  gruen  10236  intgru  10238  grudomon  10241  grur1a  10243  grutsk1  10245  nqereu  10353  nqereq  10359  ltsonq  10393  prlem934  10457  reclem3pr  10473  1re  10643  axsup  10718  addid2  10825  recex  11274  lemul1a  11496  lt2msq  11527  fimaxre2  11588  zdiv  12055  zextlt  12059  prime  12066  uzind2  12078  fzind  12083  lbzbi  12339  qbtwnxr  12596  qextltlem  12598  xralrple  12601  xltneg  12613  xlt2add  12656  supxrgtmnf  12725  ixxub  12762  ixxlb  12763  ioo0  12766  ico0  12787  ioc0  12788  icc0  12789  iocssre  12819  icossre  12820  iccssre  12821  fzen  12927  expclzlem  13456  expaddz  13476  expmulz  13478  hashgadd  13741  hashunsngx  13757  hashgt23el  13788  elovmpowrd  13912  pfxnd0  14052  ccatopth2  14081  pfxccatin12  14097  cshf1  14174  shftuz  14430  cau3lem  14716  caubnd  14720  climuni  14911  lo1resb  14923  o1resb  14925  o1of2  14971  o1add  14972  o1mul  14973  o1sub  14974  ntrivcvgmul  15260  eflt  15472  moddvds  15620  dvdscmulr  15640  dvdsmulcr  15641  dvdsle  15662  divalglem8  15753  divalgb  15757  ndvdssub  15762  bitsfzo  15786  gcdcllem1  15850  gcdcllem3  15852  dvdsgcd  15894  lcmgcdlem  15952  lcmfeq0b  15976  qredeu  16004  isprm3  16029  prmdvdsexpr  16063  prmexpb  16064  eulerthlem2  16121  fermltl  16123  coprimeprodsq  16147  pythagtrip  16173  pcprendvds  16179  pcpremul  16182  pcdvdsb  16207  pc2dvds  16217  4sqlem12  16294  4sqlem18  16300  vdwlem10  16328  cshwshashlem3  16433  xpsrnbas  16846  ismred  16875  mrieqv2d  16912  iscatd  16946  isfuncd  17137  fthestrcsetc  17402  fthsetcestrc  17417  poslubd  17760  dirtr  17848  mulgaddcom  18253  ghmrn  18373  pmtrprfv3  18584  mndodcongi  18673  oddvdsnn0  18674  oddvds  18677  odcl2  18694  odhash3  18703  gexdvds  18711  pgpfi  18732  lsmss1b  18794  lsmss2b  18796  efgsrel  18862  efgred  18876  cntzcmn  18962  cyggenod  19005  lt6abl  19017  gsumcom2  19097  pgpfac1lem2  19199  pgpfac1lem3  19201  dvdsunit  19415  unitmulclb  19417  irredrmul  19459  isabvd  19593  lmodvsdi  19659  lss0cl  19720  islbs3  19929  lbsextlem2  19933  mvrf1  20207  coe1fzgsumd  20472  gsummoncoe1  20474  evl1gsumd  20522  xrsdsreclblem  20593  scmataddcl  21127  scmatsubcl  21128  mdetunilem9  21231  mdetuni0  21232  mdetmul  21234  m2cpmrngiso  21368  pm2mpf1  21409  opnnei  21730  neindisj2  21733  cncls2  21883  cncls  21884  cnntr  21885  cnpresti  21898  cnprest  21899  lmcnp  21914  isreg2  21987  ordthauslem  21993  unconn  22039  2ndc1stc  22061  kgen2ss  22165  ptclsg  22225  cnmptcom  22288  kqfvima  22340  hmeof1o  22374  fbncp  22449  fbfinnfr  22451  trfbas2  22453  isufil2  22518  ufprim  22519  trufil  22520  filufint  22530  hausflim  22591  flimrest  22593  flimcls  22595  cnpfcf  22651  alexsubALT  22661  tmdgsum  22705  opnsubg  22718  cldsubg  22721  qustgpopn  22730  tsmsxp  22765  blpnf  23009  blssps  23036  blss  23037  blssec  23047  neibl  23113  prdsxmslem2  23141  xrsmopn  23422  metnrm  23472  climcncf  23510  iccpnfhmeo  23551  xrhmeo  23552  bndth  23564  cphsqrtcl3  23793  iscau2  23882  iscmet3lem2  23897  bcthlem5  23933  bcth3  23936  ishl2  23975  ivthlem1  24054  cmmbl  24137  iundisj2  24152  voliunlem2  24154  mbfaddlem  24263  itg2itg1  24339  itg2seq  24345  itg2mulclem  24349  cnplimc  24487  dvres2  24512  deg1nn0clb  24686  deg1lt0  24687  deg1ge  24694  plypf1  24804  plyadd  24809  plymul  24810  coeeu  24817  dgrub2  24827  coeidlem  24829  coeid3  24832  coemullem  24842  coe11  24845  coemulhi  24846  coemulc  24847  dgreq0  24857  dgrlt  24858  dgradd2  24860  vieta1lem2  24902  tanord1  25123  tanord  25124  logccne0  25164  cxpeq0  25263  cxpmul2z  25276  cxpcn3lem  25330  relogbzcl  25354  angpieqvd  25411  o1cxp  25554  scvxcvx  25565  chtublem  25789  bposlem3  25864  lgsqr  25929  2sqnn  26017  dchrisumlema  26066  dchrisumlem2  26068  ostth2lem3  26213  tghilberti2  26426  inagswap  26629  f1otrg  26659  brbtwn2  26693  axpasch  26729  axcontlem4  26755  axcontlem5  26756  upgredg2vtx  26928  usgredg2vtxeuALT  27006  sizusglecusg  27247  upgredginwlk  27419  frgrwopreg1  28099  frgrwopreg2  28100  frgrregorufrg  28107  lpni  28259  ipasslem5  28614  htthlem  28696  omlsii  29182  spansni  29336  spansneleq  29349  elspansn4  29352  sumspansn  29428  homco1  29580  homulass  29581  mdsl0  30089  ssdmd1  30092  ssdmd2  30093  cvdmd  30116  chirredlem2  30170  atdmd  30177  atmd2  30179  disjif  30330  iundisj2f  30342  isoun  30439  padct  30457  iocinioc2  30504  iundisj2fi  30522  archiabllem1a  30822  archiabllem2a  30825  slmdvsdi  30845  ordtconnlem1  31169  indpi1  31281  measinblem  31481  measres  31483  measdivcstALTV  31486  mbfmco2  31525  orvclteinc  31735  sgn3da  31801  sgnnbi  31805  sgnpbi  31806  bnj605  32181  bnj607  32190  bnj964  32217  bnj1033  32243  bnj1128  32264  bnj1137  32269  bnj1136  32271  bnj1413  32309  bnj60  32336  cusgredgex  32370  subgrwlk  32381  acycgr1v  32398  cvmlift2lem10  32561  msubvrs  32809  wsuclem  33114  nosepon  33174  noextenddif  33177  nolesgn2o  33180  nosepne  33187  nodense  33198  dfrdg4  33414  brcolinear2  33521  brsegle2  33572  nn0prpw  33673  ntruni  33677  clsint2  33679  fnessref  33707  fnemeet2  33717  fnejoin2  33719  limsucncmpi  33795  ee7.2aOLD  33811  bj-idreseq  34456  dissneqlem  34623  isbasisrelowllem1  34638  isbasisrelowllem2  34639  icoreclin  34640  poimirlem9  34903  poimirlem30  34924  poimirlem32  34926  areacirc  34989  filbcmb  35017  mettrifi  35034  heiborlem8  35098  heiborlem10  35100  heibor  35101  riscer  35268  igenval2  35346  lshpcmp  36126  eqlkr  36237  lkrlsp2  36241  lkrshp  36243  cvrnbtwn2  36413  cvlexch3  36470  cvlexch4N  36471  cvlatexchb1  36472  cvlsupr3  36482  exatleN  36542  cvratlem  36559  atcvrj2b  36570  cvrat3  36580  cvrat4  36581  athgt  36594  ps-1  36615  ps-2  36616  3atlem5  36625  3at  36628  llnneat  36652  llnmlplnN  36677  lplnneat  36683  lplnnelln  36684  islpln2a  36686  lplnriaN  36688  lplnribN  36689  lplnexllnN  36702  2llnjaN  36704  lvolnle3at  36720  lvolneatN  36726  lvolnelln  36727  lvolnelpln  36728  islvol2aN  36730  dalem62  36872  pmapglb2N  36909  pmapglb2xN  36910  lncmp  36921  paddasslem14  36971  paddasslem15  36972  pmod2iN  36987  hlmod1i  36994  pclfinclN  37088  osumcllem8N  37101  pexmidlem4N  37111  pl42lem1N  37117  pl42lem4N  37120  lhpexle1  37146  lhpexle2lem  37147  lhpmcvr5N  37165  lhpmcvr6N  37166  ltrneq  37287  trlnidatb  37315  cdleme0ex2N  37362  cdleme27a  37505  cdleme17d3  37634  cdlemeg46gfre  37670  cdleme48gfv1  37674  cdlemeg49lebilem  37677  cdlemf2  37700  cdlemf  37701  cdlemfnid  37702  trlord  37707  cdlemg31c  37837  cdlemg35  37851  trlcone  37866  tendoeq2  37912  cdlemj3  37961  cdlemk26b-3  38043  cdlemk33N  38047  cdleml3N  38116  cdlemn  38350  dih1dimb2  38379  dihord5apre  38400  dihmeetlem1N  38428  dihglblem5apreN  38429  dihglblem2N  38432  dihglblem3N  38433  dihmeetlem13N  38457  dihmeetlem15N  38459  dihatexv  38476  hdmap14lem12  39017  frlmfzowrdb  39150  nn0rppwr  39189  nn0expgcd  39191  rtprmirr  39201  oddcomabszz  39548  jm2.19lem4  39596  fiuneneq  39804  idomsubgmo  39805  pwinfi3  39929  gneispa  40487  grumnudlem  40628  binomcxplemnn0  40688  addrcom  40814  int3  40953  suctrALT  41167  suctrALTcf  41263  suctrALT3  41265  chordthmALT  41274  iunconnlem2  41276  stoweidlem26  42318  stoweidlem34  42326  issald  42623  goldbachth  43716  nnsgrp  44091  ply1mulgsumlem1  44447