Theorem 3expia 1127

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

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

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 1094

This theorem is referenced by:  ad5ant125  1374  mp3an3  1458  3gencl  3474  vtocl3gaf  3523  vtocl3ga  3524  moi  3659  disji  5057  disjord  5061  3optocl  5715  sossfld  6137  f1oresrab  7069  f1cdmsn  7226  soisores  7271  isomin  7281  isofrlem  7284  ovmpos  7504  ov2gf  7505  ndmovord  7546  nnsuc  7824  poxp  8068  frpoins3xp3g  8081  brtpos  8175  dfsmo2  8277  smoiun  8291  smoord  8295  smogt  8297  omeulem1  8507  omeu  8510  oewordi  8517  uniinqs  8734  mapvalg  8773  pmvalg  8774  elmapg  8776  xpdom3  9003  mapdom3  9077  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  nndomog  9137  onomeneq  9138  sucdom  9144  unxpdomlem3  9158  isinf  9165  f1finf1o  9173  isfinite2  9198  prfi  9224  ordiso  9421  cnfcom3clem  9617  r111  9690  tskwe  9865  pr2ne  9918  infxpenlem  9926  dfac8alem  9942  infdif  10121  infdif2  10122  cff1  10171  coflim  10174  cfslbn  10180  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  fin23lem27  10241  isf32lem9  10274  isf34lem6  10293  axcc2lem  10349  domtriomlem  10355  axdc4lem  10368  zorn2lem2  10410  axdclem2  10433  konigthlem  10482  gchen1  10539  gchen2  10540  gchpwdom  10584  gchaleph  10585  winainflem  10607  tskcard  10695  gruiun  10713  gruen  10726  intgru  10728  grudomon  10731  grur1a  10733  grutsk1  10735  nqereu  10843  nqereq  10849  ltsonq  10883  prlem934  10947  reclem3pr  10963  1re  11135  axsup  11212  addlid  11320  recex  11773  lemul1a  12000  lt2msq  12032  fimaxre2  12092  indpi1  12164  zdiv  12590  zextlt  12594  prime  12601  uzind2  12613  fzind  12618  lbzbi  12877  qbtwnxr  13143  qextltlem  13145  xralrple  13148  xltneg  13160  xlt2add  13203  supxrgtmnf  13272  ixxub  13310  ixxlb  13311  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  iocssre  13371  icossre  13372  iccssre  13373  fzen  13486  expclzlem  14036  expaddz  14059  expmulz  14061  hashgadd  14330  hashunsngx  14346  hashgt23el  14377  elovmpowrd  14511  pfxnd0  14642  ccatopth2  14670  pfxccatin12  14686  cshf1  14763  shftuz  15022  cau3lem  15308  caubnd  15312  climuni  15505  lo1resb  15517  o1resb  15519  o1of2  15566  o1add  15567  o1mul  15568  o1sub  15569  ntrivcvgmul  15858  eflt  16075  moddvds  16223  dvdscmulr  16244  dvdsmulcr  16245  dvdsle  16270  divalglem8  16360  divalgb  16364  ndvdssub  16369  bitsfzo  16395  gcdcllem1  16459  gcdcllem3  16461  dvdsgcd  16504  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  lcmfeq0b  16590  qredeu  16618  isprm3  16643  prmdvdsexpr  16678  prmexpb  16680  eulerthlem2  16743  fermltl  16745  coprimeprodsq  16770  pythagtrip  16796  pcprendvds  16802  pcpremul  16805  pcdvdsb  16831  pc2dvds  16841  4sqlem12  16918  4sqlem18  16924  vdwlem10  16952  cshwshashlem3  17059  xpsrnbas  17526  ismred  17555  mrieqv2d  17596  iscatd  17630  isfuncd  17823  fthestrcsetc  18107  fthsetcestrc  18122  poslubd  18368  dirtr  18559  mulgaddcom  19065  ghmrn  19195  pmtrprfv3  19420  mndodcongi  19509  oddvdsnn0  19510  oddvds  19513  odcl2  19531  odhash3  19542  gexdvds  19550  pgpfi  19571  lsmss1b  19632  lsmss2b  19634  efgsrel  19700  efgred  19714  cntzcmn  19806  cyggenod  19850  lt6abl  19861  gsumcom2  19941  pgpfac1lem2  20043  pgpfac1lem3  20045  dvdsunit  20350  unitmulclb  20352  irredrmul  20398  isabvd  20784  lmodvsdi  20875  lss0cl  20937  islbs3  21148  lbsextlem2  21152  xrsdsreclblem  21388  psrbaglefi  21901  mvrf1  21960  coe1fzgsumd  22290  gsummoncoe1  22294  evl1gsumd  22343  scmataddcl  22499  scmatsubcl  22500  mdetunilem9  22603  mdetuni0  22604  mdetmul  22606  m2cpmrngiso  22741  pm2mpf1  22782  opnnei  23103  neindisj2  23106  cncls2  23256  cncls  23257  cnntr  23258  cnpresti  23271  cnprest  23272  lmcnp  23287  isreg2  23360  ordthauslem  23366  unconn  23412  2ndc1stc  23434  kgen2ss  23538  ptclsg  23598  cnmptcom  23661  kqfvima  23713  hmeof1o  23747  fbncp  23822  fbfinnfr  23824  trfbas2  23826  isufil2  23891  ufprim  23892  trufil  23893  filufint  23903  hausflim  23964  flimrest  23966  flimcls  23968  cnpfcf  24024  alexsubALT  24034  tmdgsum  24078  opnsubg  24091  cldsubg  24094  qustgpopn  24103  tsmsxp  24138  blpnf  24380  blssps  24407  blss  24408  blssec  24418  neibl  24484  prdsxmslem2  24512  xrsmopn  24796  metnrm  24846  climcncf  24885  iccpnfhmeo  24930  xrhmeo  24931  bndth  24943  cphsqrtcl3  25172  iscau2  25262  iscmet3lem2  25277  bcthlem5  25313  bcth3  25316  ishl2  25355  ivthlem1  25436  cmmbl  25519  iundisj2  25534  voliunlem2  25536  mbfaddlem  25645  itg2itg1  25721  itg2seq  25727  itg2mulclem  25731  cnplimc  25872  dvres2  25897  deg1nn0clb  26073  deg1lt0  26074  deg1ge  26081  plypf1  26195  plyadd  26200  plymul  26201  coeeu  26208  dgrub2  26218  coeidlem  26220  coeid3  26223  coemullem  26233  coe11  26236  coemulhi  26237  coemulc  26238  dgreq0  26248  dgrlt  26249  dgradd2  26251  vieta1lem2  26295  tanord1  26519  tanord  26520  logccne0  26560  cxpeq0  26660  cxpmul2z  26673  cxpcn3lem  26729  rtprmirr  26742  relogbzcl  26756  angpieqvd  26813  o1cxp  26956  scvxcvx  26967  chtublem  27192  bposlem3  27267  lgsqr  27332  2sqnn  27420  dchrisumlema  27469  dchrisumlem2  27471  ostth2lem3  27616  nosepon  27647  noextenddif  27650  nolesgn2o  27653  nogesgn1o  27655  nosepne  27662  nodense  27674  onnolt  28276  onlts  28277  oniso  28281  bdayn0p1  28379  bdayn0sf1o  28380  tghilberti2  28724  inagswap  28927  f1otrg  28957  brbtwn2  28992  axpasch  29028  axcontlem4  29054  axcontlem5  29055  upgredg2vtx  29228  usgredg2vtxeuALT  29309  sizusglecusg  29550  upgredginwlk  29722  frgrwopreg1  30406  frgrwopreg2  30407  frgrregorufrg  30414  lpni  30569  ipasslem5  30924  htthlem  31006  omlsii  31492  spansni  31646  spansneleq  31659  elspansn4  31662  sumspansn  31738  homco1  31890  homulass  31891  mdsl0  32399  ssdmd1  32402  ssdmd2  32403  cvdmd  32426  chirredlem2  32480  atdmd  32487  atmd2  32489  disjif  32667  iundisj2f  32679  isoun  32794  preiman0  32802  padct  32810  iocinioc2  32871  iundisj2fi  32889  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  archiabllem1a  33272  archiabllem2a  33275  slmdvsdi  33296  ordtconnlem1  34108  measinblem  34404  measres  34406  measdivcstALTV  34409  mbfmco2  34449  orvclteinc  34660  bnj605  35089  bnj607  35098  bnj964  35125  bnj1033  35151  bnj1128  35172  bnj1137  35177  bnj1136  35179  bnj1413  35217  bnj60  35244  rankfilimb  35283  r1filim  35285  fineqvac  35297  fineqvnttrclselem3  35304  fineqvnttrclse  35305  cusgredgex  35350  subgrwlk  35360  acycgr1v  35377  cvmlift2lem10  35540  msubvrs  35788  wsuclem  36051  dfrdg4  36179  brcolinear2  36286  brsegle2  36337  nn0prpw  36551  ntruni  36555  clsint2  36557  fnessref  36585  fnemeet2  36595  fnejoin2  36597  limsucncmpi  36673  ee7.2aOLD  36689  bj-idreseq  37522  dissneqlem  37702  isbasisrelowllem1  37717  isbasisrelowllem2  37718  icoreclin  37719  poimirlem9  37996  poimirlem30  38017  poimirlem32  38019  areacirc  38080  filbcmb  38107  mettrifi  38124  heiborlem8  38185  heiborlem10  38187  heibor  38188  riscer  38355  igenval2  38433  eldisjim3  39182  eldisjs6  39307  lshpcmp  39480  eqlkr  39591  lkrlsp2  39595  lkrshp  39597  cvrnbtwn2  39767  cvlexch3  39824  cvlexch4N  39825  cvlatexchb1  39826  cvlsupr3  39836  exatleN  39896  cvratlem  39913  atcvrj2b  39924  cvrat3  39934  cvrat4  39935  athgt  39948  ps-1  39969  ps-2  39970  3atlem5  39979  3at  39982  llnneat  40006  llnmlplnN  40031  lplnneat  40037  lplnnelln  40038  islpln2a  40040  lplnriaN  40042  lplnribN  40043  lplnexllnN  40056  2llnjaN  40058  lvolnle3at  40074  lvolneatN  40080  lvolnelln  40081  lvolnelpln  40082  islvol2aN  40084  dalem62  40226  pmapglb2N  40263  pmapglb2xN  40264  lncmp  40275  paddasslem14  40325  paddasslem15  40326  pmod2iN  40341  hlmod1i  40348  pclfinclN  40442  osumcllem8N  40455  pexmidlem4N  40465  pl42lem1N  40471  pl42lem4N  40474  lhpexle1  40500  lhpexle2lem  40501  lhpmcvr5N  40519  lhpmcvr6N  40520  ltrneq  40641  trlnidatb  40669  cdleme0ex2N  40716  cdleme27a  40859  cdleme17d3  40988  cdlemeg46gfre  41024  cdleme48gfv1  41028  cdlemeg49lebilem  41031  cdlemf2  41054  cdlemf  41055  cdlemfnid  41056  trlord  41061  cdlemg31c  41191  cdlemg35  41205  trlcone  41220  tendoeq2  41266  cdlemj3  41315  cdlemk26b-3  41397  cdlemk33N  41401  cdleml3N  41470  cdlemn  41704  dih1dimb2  41733  dihord5apre  41754  dihmeetlem1N  41782  dihglblem5apreN  41783  dihglblem2N  41786  dihglblem3N  41787  dihmeetlem13N  41811  dihmeetlem15N  41813  dihatexv  41830  hdmap14lem12  42371  uzindd  42463  lcmineqlem1  42514  sticksstones1  42631  dvdsexpnn0  42811  frlmfzowrdb  42994  oddcomabszz  43389  jm2.19lem4  43437  fiuneneq  43637  idomsubgmo  43638  omcl2  43778  pwinfi3  44007  gneispa  44574  mnringmulrcld  44672  grumnudlem  44729  ismnushort  44745  binomcxplemnn0  44793  addrcom  44918  int3  45056  suctrALT  45269  suctrALTcf  45365  suctrALT3  45367  chordthmALT  45376  iunconnlem2  45378  relpmin  45396  relpfrlem  45397  stoweidlem26  46469  stoweidlem34  46477  issald  46776  goldbachth  48025  nprmdvdsfacm1  48102  grlimgrtri  48494  nnsgrp  48668  ply1mulgsumlem1  48877  lubsscl  49450  glbsscl  49451