Theorem 3expia 1114

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  ad5ant125  1359  mp3an3  1442  3gencl  3478  moi  3646  disji  4949  disjord  4953  3optocl  5536  sossfld  5922  f1oresrab  6755  soisores  6946  isomin  6956  isofrlem  6959  ovmpos  7157  ov2gf  7158  ndmovord  7197  nnsuc  7456  poxp  7678  brtpos  7755  dfsmo2  7839  smoiun  7853  smoord  7857  smogt  7859  omeulem1  8061  omeu  8064  oewordi  8070  uniinqs  8230  mapvalg  8269  pmvalg  8270  elmapg  8272  xpdom3  8465  mapdom3  8539  php3  8553  unxpdomlem3  8573  isinf  8580  findcard2  8607  isfinite2  8625  ordiso  8829  cnfcom3clem  9017  r111  9053  tskwe  9228  pr2ne  9280  infxpenlem  9288  dfac8alem  9304  infdif  9480  infdif2  9481  cff1  9529  coflim  9532  cfslbn  9538  cfslb2n  9539  cofsmo  9540  cfsmolem  9541  cfcoflem  9543  fin23lem27  9599  isf32lem9  9632  isf34lem6  9651  axcc2lem  9707  domtriomlem  9713  axdc4lem  9726  zorn2lem2  9768  axdclem2  9791  konigthlem  9839  gchen1  9896  gchen2  9897  gchpwdom  9941  gchaleph  9942  winainflem  9964  tskcard  10052  gruiun  10070  gruen  10083  intgru  10085  grudomon  10088  grur1a  10090  grutsk1  10092  nqereu  10200  nqereq  10206  ltsonq  10240  prlem934  10304  reclem3pr  10320  1re  10490  axsup  10565  addid2  10672  recex  11122  lemul1a  11344  lt2msq  11375  fimaxre2  11436  zdiv  11902  zextlt  11906  prime  11913  uzind2  11925  fzind  11930  lbzbi  12185  qbtwnxr  12443  qextltlem  12445  xralrple  12448  xltneg  12460  xlt2add  12503  supxrgtmnf  12572  ixxub  12609  ixxlb  12610  ioo0  12613  ico0  12634  ioc0  12635  icc0  12636  iocssre  12666  icossre  12667  iccssre  12668  fzen  12774  expclzlem  13303  expaddz  13323  expmulz  13325  hashgadd  13586  hashunsngx  13602  hashgt23el  13633  elovmpowrd  13756  pfxnd0  13886  ccatopth2  13915  cshf1  14008  shftuz  14262  cau3lem  14548  caubnd  14552  climuni  14743  lo1resb  14755  o1resb  14757  o1of2  14803  o1add  14804  o1mul  14805  o1sub  14806  ntrivcvgmul  15091  eflt  15303  moddvds  15451  dvdscmulr  15471  dvdsmulcr  15472  dvdsle  15493  divalglem8  15584  divalgb  15588  ndvdssub  15593  bitsfzo  15617  gcdcllem1  15681  gcdcllem3  15683  dvdsgcd  15721  lcmgcdlem  15779  lcmfeq0b  15803  qredeu  15831  isprm3  15856  prmdvdsexpr  15890  prmexpb  15891  eulerthlem2  15948  fermltl  15950  coprimeprodsq  15974  pythagtrip  16000  pcprendvds  16006  pcpremul  16009  pcdvdsb  16034  pc2dvds  16044  4sqlem12  16121  4sqlem18  16127  vdwlem10  16155  cshwshashlem3  16260  xpsrnbas  16673  ismred  16702  mrieqv2d  16739  iscatd  16773  isfuncd  16964  fthestrcsetc  17229  fthsetcestrc  17244  poslubd  17587  dirtr  17675  mulgaddcom  18005  ghmrn  18112  pmtrprfv3  18313  mndodcongi  18402  oddvdsnn0  18403  oddvds  18406  odcl2  18422  odhash3  18431  gexdvds  18439  pgpfi  18460  lsmss1b  18520  lsmss2b  18522  efgsrel  18587  efgred  18601  cntzcmn  18685  cyggenod  18726  lt6abl  18736  gsumcom2  18815  pgpfac1lem2  18914  pgpfac1lem3  18916  dvdsunit  19103  unitmulclb  19105  irredrmul  19147  isabvd  19281  lmodvsdi  19347  lss0cl  19408  islbs3  19617  lbsextlem2  19621  mvrf1  19893  coe1fzgsumd  20153  gsummoncoe1  20155  evl1gsumd  20202  xrsdsreclblem  20273  scmataddcl  20809  scmatsubcl  20810  mdetunilem9  20913  mdetuni0  20914  mdetmul  20916  m2cpmrngiso  21050  pm2mpf1  21091  opnnei  21412  neindisj2  21415  cncls2  21565  cncls  21566  cnntr  21567  cnpresti  21580  cnprest  21581  lmcnp  21596  isreg2  21669  ordthauslem  21675  unconn  21721  2ndc1stc  21743  kgen2ss  21847  ptclsg  21907  cnmptcom  21970  kqfvima  22022  hmeof1o  22056  fbncp  22131  fbfinnfr  22133  trfbas2  22135  isufil2  22200  ufprim  22201  trufil  22202  filufint  22212  hausflim  22273  flimrest  22275  flimcls  22277  cnpfcf  22333  alexsubALT  22343  tmdgsum  22387  opnsubg  22399  cldsubg  22402  qustgpopn  22411  tsmsxp  22446  blpnf  22690  blssps  22717  blss  22718  blssec  22728  neibl  22794  prdsxmslem2  22822  xrsmopn  23103  metnrm  23153  climcncf  23191  iccpnfhmeo  23232  xrhmeo  23233  bndth  23245  cphsqrtcl3  23474  iscau2  23563  iscmet3lem2  23578  bcthlem5  23614  bcth3  23617  ishl2  23656  ivthlem1  23735  cmmbl  23818  iundisj2  23833  voliunlem2  23835  mbfaddlem  23944  itg2itg1  24020  itg2seq  24026  itg2mulclem  24030  cnplimc  24168  dvres2  24193  deg1nn0clb  24367  deg1lt0  24368  deg1ge  24375  plypf1  24485  plyadd  24490  plymul  24491  coeeu  24498  dgrub2  24508  coeidlem  24510  coeid3  24513  coemullem  24523  coe11  24526  coemulhi  24527  coemulc  24528  dgreq0  24538  dgrlt  24539  dgradd2  24541  vieta1lem2  24583  tanord1  24802  tanord  24803  logccne0  24843  cxpeq0  24942  cxpmul2z  24955  cxpcn3lem  25009  relogbzcl  25033  angpieqvd  25090  o1cxp  25234  scvxcvx  25245  chtublem  25469  bposlem3  25544  lgsqr  25609  2sqnn  25697  dchrisumlema  25746  dchrisumlem2  25748  ostth2lem3  25893  tghilberti2  26106  inagswap  26310  f1otrg  26340  brbtwn2  26374  axpasch  26410  axcontlem4  26436  axcontlem5  26437  upgredg2vtx  26609  usgredg2vtxeuALT  26687  sizusglecusg  26928  upgredginwlk  27100  frgrwopreg1  27781  frgrwopreg2  27782  frgrregorufrg  27789  lpni  27940  ipasslem5  28295  htthlem  28377  omlsii  28863  spansni  29017  spansneleq  29030  elspansn4  29033  sumspansn  29109  homco1  29261  homulass  29262  mdsl0  29770  ssdmd1  29773  ssdmd2  29774  cvdmd  29797  chirredlem2  29851  atdmd  29858  atmd2  29860  disjif  30010  iundisj2f  30022  isoun  30117  padct  30135  iocinioc2  30182  iundisj2fi  30198  archiabllem1a  30450  archiabllem2a  30453  slmdvsdi  30473  ordtconnlem1  30776  indpi1  30888  measinblem  31088  measres  31090  measdivcstALTV  31093  mbfmco2  31132  orvclteinc  31342  sgn3da  31408  sgnnbi  31412  sgnpbi  31413  bnj605  31787  bnj607  31796  bnj964  31823  bnj1033  31847  bnj1128  31868  bnj1137  31873  bnj1136  31875  bnj1413  31913  bnj60  31940  cusgredgex  31972  subgrwlk  31981  acycgr1v  31998  cvmlift2lem10  32161  msubvrs  32409  wsuclem  32715  nosepon  32775  noextenddif  32778  nolesgn2o  32781  nosepne  32788  nodense  32799  dfrdg4  33015  brcolinear2  33122  brsegle2  33173  nn0prpw  33274  ntruni  33278  clsint2  33280  fnessref  33308  fnemeet2  33318  fnejoin2  33320  limsucncmpi  33396  ee7.2aOLD  33412  dissneqlem  34165  isbasisrelowllem1  34180  isbasisrelowllem2  34181  icoreclin  34182  poimirlem9  34445  poimirlem30  34466  poimirlem32  34468  areacirc  34531  filbcmb  34560  mettrifi  34577  heiborlem8  34641  heiborlem10  34643  heibor  34644  riscer  34811  igenval2  34889  lshpcmp  35668  eqlkr  35779  lkrlsp2  35783  lkrshp  35785  cvrnbtwn2  35955  cvlexch3  36012  cvlexch4N  36013  cvlatexchb1  36014  cvlsupr3  36024  exatleN  36084  cvratlem  36101  atcvrj2b  36112  cvrat3  36122  cvrat4  36123  athgt  36136  ps-1  36157  ps-2  36158  3atlem5  36167  3at  36170  llnneat  36194  llnmlplnN  36219  lplnneat  36225  lplnnelln  36226  islpln2a  36228  lplnriaN  36230  lplnribN  36231  lplnexllnN  36244  2llnjaN  36246  lvolnle3at  36262  lvolneatN  36268  lvolnelln  36269  lvolnelpln  36270  islvol2aN  36272  dalem62  36414  pmapglb2N  36451  pmapglb2xN  36452  lncmp  36463  paddasslem14  36513  paddasslem15  36514  pmod2iN  36529  hlmod1i  36536  pclfinclN  36630  osumcllem8N  36643  pexmidlem4N  36653  pl42lem1N  36659  pl42lem4N  36662  lhpexle1  36688  lhpexle2lem  36689  lhpmcvr5N  36707  lhpmcvr6N  36708  ltrneq  36829  trlnidatb  36857  cdleme0ex2N  36904  cdleme27a  37047  cdleme17d3  37176  cdlemeg46gfre  37212  cdleme48gfv1  37216  cdlemeg49lebilem  37219  cdlemf2  37242  cdlemf  37243  cdlemfnid  37244  trlord  37249  cdlemg31c  37379  cdlemg35  37393  trlcone  37408  tendoeq2  37454  cdlemj3  37503  cdlemk26b-3  37585  cdlemk33N  37589  cdleml3N  37658  cdlemn  37892  dih1dimb2  37921  dihord5apre  37942  dihmeetlem1N  37970  dihglblem5apreN  37971  dihglblem2N  37974  dihglblem3N  37975  dihmeetlem13N  37999  dihmeetlem15N  38001  dihatexv  38018  hdmap14lem12  38559  frlmfzowrdb  38683  nn0rppwr  38717  nn0expgcd  38719  rtprmirr  38729  oddcomabszz  39039  jm2.19lem4  39087  fiuneneq  39295  idomsubgmo  39296  pwinfi3  39420  gneispa  39978  grumnudlem  40131  binomcxplemnn0  40232  addrcom  40359  int3  40498  suctrALT  40712  suctrALTcf  40808  suctrALT3  40810  chordthmALT  40819  iunconnlem2  40821  stoweidlem26  41867  stoweidlem34  41875  issald  42172  goldbachth  43205  nnsgrp  43580  ply1mulgsumlem1  43934