Theorem 3expia 1121

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1368  mp3an3  1452  3gencl  3482  vtocl3gaf  3538  vtocl3ga  3540  moi  3680  disji  5080  disjord  5084  3optocl  5720  sossfld  6139  f1oresrab  7065  f1cdmsn  7223  soisores  7268  isomin  7278  isofrlem  7281  ovmpos  7501  ov2gf  7502  ndmovord  7543  nnsuc  7824  poxp  8068  frpoins3xp3g  8081  brtpos  8175  dfsmo2  8277  smoiun  8291  smoord  8295  smogt  8297  omeulem1  8507  omeu  8510  oewordi  8516  uniinqs  8731  mapvalg  8770  pmvalg  8771  elmapg  8773  xpdom3  8999  mapdom3  9073  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  nndomog  9137  onomeneq  9138  sucdom  9143  unxpdomlem3  9157  isinf  9165  isinfOLD  9166  f1finf1o  9174  isfinite2  9203  prfi  9232  ordiso  9427  cnfcom3clem  9620  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  10481  gchen1  10538  gchen2  10539  gchpwdom  10583  gchaleph  10584  winainflem  10606  tskcard  10694  gruiun  10712  gruen  10725  intgru  10727  grudomon  10730  grur1a  10732  grutsk1  10734  nqereu  10842  nqereq  10848  ltsonq  10882  prlem934  10946  reclem3pr  10962  1re  11134  axsup  11210  addlid  11318  recex  11771  lemul1a  11997  lt2msq  12029  fimaxre2  12089  zdiv  12565  zextlt  12569  prime  12576  uzind2  12588  fzind  12593  lbzbi  12856  qbtwnxr  13121  qextltlem  13123  xralrple  13126  xltneg  13138  xlt2add  13181  supxrgtmnf  13250  ixxub  13288  ixxlb  13289  ioo0  13292  ico0  13313  ioc0  13314  icc0  13315  iocssre  13349  icossre  13350  iccssre  13351  fzen  13463  expclzlem  14009  expaddz  14032  expmulz  14034  hashgadd  14303  hashunsngx  14319  hashgt23el  14350  elovmpowrd  14484  pfxnd0  14614  ccatopth2  14642  pfxccatin12  14658  cshf1  14735  shftuz  14995  cau3lem  15281  caubnd  15285  climuni  15478  lo1resb  15490  o1resb  15492  o1of2  15539  o1add  15540  o1mul  15541  o1sub  15542  ntrivcvgmul  15828  eflt  16045  moddvds  16193  dvdscmulr  16214  dvdsmulcr  16215  dvdsle  16240  divalglem8  16330  divalgb  16334  ndvdssub  16339  bitsfzo  16365  gcdcllem1  16429  gcdcllem3  16431  dvdsgcd  16474  nn0rppwr  16491  nn0expgcd  16494  lcmgcdlem  16536  lcmfeq0b  16560  qredeu  16588  isprm3  16613  prmdvdsexpr  16647  prmexpb  16649  eulerthlem2  16712  fermltl  16714  coprimeprodsq  16739  pythagtrip  16765  pcprendvds  16771  pcpremul  16774  pcdvdsb  16800  pc2dvds  16810  4sqlem12  16887  4sqlem18  16893  vdwlem10  16921  cshwshashlem3  17028  xpsrnbas  17494  ismred  17523  mrieqv2d  17564  iscatd  17598  isfuncd  17791  fthestrcsetc  18075  fthsetcestrc  18090  poslubd  18336  dirtr  18527  mulgaddcom  18996  ghmrn  19127  pmtrprfv3  19352  mndodcongi  19441  oddvdsnn0  19442  oddvds  19445  odcl2  19463  odhash3  19474  gexdvds  19482  pgpfi  19503  lsmss1b  19564  lsmss2b  19566  efgsrel  19632  efgred  19646  cntzcmn  19738  cyggenod  19782  lt6abl  19793  gsumcom2  19873  pgpfac1lem2  19975  pgpfac1lem3  19977  dvdsunit  20283  unitmulclb  20285  irredrmul  20331  isabvd  20716  lmodvsdi  20807  lss0cl  20869  islbs3  21081  lbsextlem2  21085  xrsdsreclblem  21338  psrbaglefi  21852  mvrf1  21912  coe1fzgsumd  22208  gsummoncoe1  22212  evl1gsumd  22261  scmataddcl  22420  scmatsubcl  22421  mdetunilem9  22524  mdetuni0  22525  mdetmul  22527  m2cpmrngiso  22662  pm2mpf1  22703  opnnei  23024  neindisj2  23027  cncls2  23177  cncls  23178  cnntr  23179  cnpresti  23192  cnprest  23193  lmcnp  23208  isreg2  23281  ordthauslem  23287  unconn  23333  2ndc1stc  23355  kgen2ss  23459  ptclsg  23519  cnmptcom  23582  kqfvima  23634  hmeof1o  23668  fbncp  23743  fbfinnfr  23745  trfbas2  23747  isufil2  23812  ufprim  23813  trufil  23814  filufint  23824  hausflim  23885  flimrest  23887  flimcls  23889  cnpfcf  23945  alexsubALT  23955  tmdgsum  23999  opnsubg  24012  cldsubg  24015  qustgpopn  24024  tsmsxp  24059  blpnf  24302  blssps  24329  blss  24330  blssec  24340  neibl  24406  prdsxmslem2  24434  xrsmopn  24718  metnrm  24768  climcncf  24810  iccpnfhmeo  24860  xrhmeo  24861  bndth  24874  cphsqrtcl3  25104  iscau2  25194  iscmet3lem2  25209  bcthlem5  25245  bcth3  25248  ishl2  25287  ivthlem1  25369  cmmbl  25452  iundisj2  25467  voliunlem2  25469  mbfaddlem  25578  itg2itg1  25654  itg2seq  25660  itg2mulclem  25664  cnplimc  25805  dvres2  25830  deg1nn0clb  26012  deg1lt0  26013  deg1ge  26020  plypf1  26134  plyadd  26139  plymul  26140  coeeu  26147  dgrub2  26157  coeidlem  26159  coeid3  26162  coemullem  26172  coe11  26175  coemulhi  26176  coemulc  26177  dgreq0  26188  dgrlt  26189  dgradd2  26191  vieta1lem2  26236  tanord1  26463  tanord  26464  logccne0  26504  cxpeq0  26604  cxpmul2z  26617  cxpcn3lem  26674  rtprmirr  26687  relogbzcl  26701  angpieqvd  26758  o1cxp  26902  scvxcvx  26913  chtublem  27139  bposlem3  27214  lgsqr  27279  2sqnn  27367  dchrisumlema  27416  dchrisumlem2  27418  ostth2lem3  27563  nosepon  27594  noextenddif  27597  nolesgn2o  27600  nogesgn1o  27602  nosepne  27609  nodense  27621  onnolt  28191  onslt  28192  onsiso  28193  bdayn0p1  28282  bdayn0sf1o  28283  tghilberti2  28602  inagswap  28805  f1otrg  28835  brbtwn2  28869  axpasch  28905  axcontlem4  28931  axcontlem5  28932  upgredg2vtx  29105  usgredg2vtxeuALT  29186  sizusglecusg  29428  upgredginwlk  29600  frgrwopreg1  30281  frgrwopreg2  30282  frgrregorufrg  30289  lpni  30443  ipasslem5  30798  htthlem  30880  omlsii  31366  spansni  31520  spansneleq  31533  elspansn4  31536  sumspansn  31612  homco1  31764  homulass  31765  mdsl0  32273  ssdmd1  32276  ssdmd2  32277  cvdmd  32300  chirredlem2  32354  atdmd  32361  atmd2  32363  disjif  32541  iundisj2f  32553  isoun  32663  preiman0  32671  padct  32681  iocinioc2  32741  iundisj2fi  32759  sgn3da  32798  sgnnbi  32802  sgnpbi  32803  indpi1  32822  archiabllem1a  33152  archiabllem2a  33155  slmdvsdi  33176  ordtconnlem1  33910  measinblem  34206  measres  34208  measdivcstALTV  34211  mbfmco2  34252  orvclteinc  34463  bnj605  34893  bnj607  34902  bnj964  34929  bnj1033  34955  bnj1128  34976  bnj1137  34981  bnj1136  34983  bnj1413  35021  bnj60  35048  fineqvac  35091  cusgredgex  35114  subgrwlk  35124  acycgr1v  35141  cvmlift2lem10  35304  msubvrs  35552  wsuclem  35818  dfrdg4  35944  brcolinear2  36051  brsegle2  36102  nn0prpw  36316  ntruni  36320  clsint2  36322  fnessref  36350  fnemeet2  36360  fnejoin2  36362  limsucncmpi  36438  ee7.2aOLD  36454  bj-idreseq  37155  dissneqlem  37333  isbasisrelowllem1  37348  isbasisrelowllem2  37349  icoreclin  37350  poimirlem9  37628  poimirlem30  37649  poimirlem32  37651  areacirc  37712  filbcmb  37739  mettrifi  37756  heiborlem8  37817  heiborlem10  37819  heibor  37820  riscer  37987  igenval2  38065  lshpcmp  38986  eqlkr  39097  lkrlsp2  39101  lkrshp  39103  cvrnbtwn2  39273  cvlexch3  39330  cvlexch4N  39331  cvlatexchb1  39332  cvlsupr3  39342  exatleN  39403  cvratlem  39420  atcvrj2b  39431  cvrat3  39441  cvrat4  39442  athgt  39455  ps-1  39476  ps-2  39477  3atlem5  39486  3at  39489  llnneat  39513  llnmlplnN  39538  lplnneat  39544  lplnnelln  39545  islpln2a  39547  lplnriaN  39549  lplnribN  39550  lplnexllnN  39563  2llnjaN  39565  lvolnle3at  39581  lvolneatN  39587  lvolnelln  39588  lvolnelpln  39589  islvol2aN  39591  dalem62  39733  pmapglb2N  39770  pmapglb2xN  39771  lncmp  39782  paddasslem14  39832  paddasslem15  39833  pmod2iN  39848  hlmod1i  39855  pclfinclN  39949  osumcllem8N  39962  pexmidlem4N  39972  pl42lem1N  39978  pl42lem4N  39981  lhpexle1  40007  lhpexle2lem  40008  lhpmcvr5N  40026  lhpmcvr6N  40027  ltrneq  40148  trlnidatb  40176  cdleme0ex2N  40223  cdleme27a  40366  cdleme17d3  40495  cdlemeg46gfre  40531  cdleme48gfv1  40535  cdlemeg49lebilem  40538  cdlemf2  40561  cdlemf  40562  cdlemfnid  40563  trlord  40568  cdlemg31c  40698  cdlemg35  40712  trlcone  40727  tendoeq2  40773  cdlemj3  40822  cdlemk26b-3  40904  cdlemk33N  40908  cdleml3N  40977  cdlemn  41211  dih1dimb2  41240  dihord5apre  41261  dihmeetlem1N  41289  dihglblem5apreN  41290  dihglblem2N  41293  dihglblem3N  41294  dihmeetlem13N  41318  dihmeetlem15N  41320  dihatexv  41337  hdmap14lem12  41878  uzindd  41970  lcmineqlem1  42022  sticksstones1  42139  dvdsexpnn0  42327  frlmfzowrdb  42497  oddcomabszz  42937  jm2.19lem4  42985  fiuneneq  43185  idomsubgmo  43186  omcl2  43326  pwinfi3  43556  gneispa  44123  mnringmulrcld  44221  grumnudlem  44278  ismnushort  44294  binomcxplemnn0  44342  addrcom  44468  int3  44606  suctrALT  44819  suctrALTcf  44915  suctrALT3  44917  chordthmALT  44926  iunconnlem2  44928  relpmin  44946  relpfrlem  44947  stoweidlem26  46027  stoweidlem34  46035  issald  46334  goldbachth  47551  grlimgrtri  48007  nnsgrp  48181  ply1mulgsumlem1  48391  lubsscl  48964  glbsscl  48965